Inference at * 2 
Iof proof for Lemma inconsistent-bool-eq3:



1. b : 
2. (b)
  (ff = tt)  False 

latex

 by (RWO "inconsistent-bool-eq2" 0) 
CollapseTHEN (Auto) 

latex

C.

Definitions	x:A. B(x), x:A  B(x), x:AB(x), , s = t, , ff, tt, t  T, P  Q, P & Q, P  Q, P  Q, False
Lemmas	iff functionality wrt iff, inconsistent-bool-eq2, bool wf, bfalse wf, btrue wf, false wf